\begin{tabbing}
d{-}chooser($D$;${\it dec}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$j$, $b$:Id, $s$:M($j$).state.\+
\\[0ex](isl(${\it dec}$($j$,$b$,$s$)) $\Leftrightarrow$ $b$ in dom(M($j$).pre) \& ($\exists$$v$:M($j$).da(locl($b$)). M($j$).pre($b$,$s$,$v$)))
\\[0ex]\& (isl(${\it dec}$($j$,$b$,$s$)) $\Rightarrow$ $b$ in dom(M($j$).pre) \& M($j$).pre($b$,$s$,outl(${\it dec}$($j$,$b$,$s$))))
\-
\end{tabbing}